T,X:Type, eq:EqDecider(X), f,g:fpf(X; x.Type), x:X.
fpf-sub(X; x.Type; eq; f; g)  subtype_rel(fpf-cap(f; eq; x; void); fpf-cap(g; eq; x; T)) 

latex

Definitions	x:A. B(x), P  Q, fpf-cap(f; eq; x; z), t  T, if b then t else f fi , x. t(x), tt, ff, prop{i:l}, , x(s), Unit, P  Q, P  Q, fpf-sub(A; a.B(a); eq; f; g), A c B, A, False,
Lemmas	fpf-dom wf, fpf-trivial-subtype-top, bool wf, eqtt to assert, fpf-ap wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-cap wf, fpf-sub wf, fpf wf, deq wf